\begin{tabbing}
at src($l$):
\\[0ex]action \$a(m) 
\\[0ex]p\=recondition $P$\+
\\[0ex]sends [\$tg,$f$] on link $l$
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$([\=Rpre(source($l$);${\it ds}$;"\$a";$p$;$P$); \+
\\[0ex]
\\[0ex]Rsends(${\it ds}$;locl("\$a");Outcome;$l$;"\$tg" : $T$;[$<$"\$tg", $\lambda$$s$,$v$. [($f$($s$,$v$))]$>$]);
\\[0ex]
\\[0ex]Rsframe($l$;"\$tg";[locl("\$a")])])
\-
\end{tabbing}